Nuprl Lemma : fpf-join-list-domain2 11,40

A:Type, eq:EqDecider(A), L:(a:A fp Top List), x:A.
(x  fpf-domain((L)))  (fL.(x  fpf-domain(f))) 
latex


Definitionst  T, x:AB(x), x:AB(x), (x  l), Top, a:A fp B(a), (xL.P(x)), P  Q, xt(x), type List, EqDecider(T), Type, x:A  B(x), P & Q, b, x  dom(f), , A c B, x:AB(x), fpf-domain(f), P  Q, P  Q, x.A(x), (L)
Lemmasiff functionality wrt iff, member-fpf-domain, fpf-join-list wf, l exists wf, fpf-domain wf, l member wf, assert wf, fpf-dom wf, fpf-join-list-dom2, deq wf, fpf wf, top wf

origin